| Definitions |  x:A. B(x),  x:A. B(x), finite-type(T), x:A B(x), P & Q, Feasible(D), Dsys, t  T, Id, Unit,  , IdLnk, left+right, x:A  B(x), s = t,  b, a<b, Void, A & B, M(i), a in dom(M.pre), P   Q, False,  A, A B, f(a), 1of(t), upto(n), 2of(t), map(f;as),  x.A(x), type List, source(l), M sends on link l, Type, destination(l), {x:A| B(x) }, #$n, {i..j }, Surj(A; B; f),  x. t(x), Prop, S  T,  , a:A fp B(a), M.din(l,tg), M.dout(l,tg), Valtype(da;k), MsgA, inr(x), inl(x), as @ bs, (x l), null(as),  x:A. B(x), Top,  , if b t else f fi, nil, b,  , P  Q, false, s ~ t, {T}, SQType(T), Case b of inl(x) s(x) ; inr(y) t(y), <a,b>, S  T, P Q, i j < k, x dom(f), IdDeq, EqDecider(T), deq-member(eq;x;L), tl(l), n-m, if a<b c ; d fi, i<j, ij, nth_tl(n;as), hd(l), l[i], n+m, Case of a; nil s ; x.y, rec:z t(x;y;z), Y, ||as||, Atom, P  Q, Dec(P), True,  T, outl(x), isl(x), outr(x) |
| Lemmas | true wf, outr wf, isl wf, outl wf, length wf1, select wf, member upto, int seg properties, member map, member append, nil member, decidable false, assert-deq-member, deq-member wf, false wf, id-deq wf, upto is nil, implies functionality wrt iff, nat properties, map is nil, ma-has-pre wf, append is nil, unit wf, l member wf, le wf, it wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of null, bool wf, bnot wf, not wf, null wf3, top wf, round-robin, append wf, msga wf, map wf, pi2 wf, upto wf, pi1 wf, surject wf, int seg wf, nat wf, subtype rel list, ldst wf, assert wf, ma-sends-on wf, d-m wf, lsrc wf, IdLnk wf, Id wf, d-feasible wf, dsys wf |
